\begin{tabbing}
ma{-}interface{-}consistent2(${\it es}$;$I$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:Id.\+
\\[0ex]($i$ $\in$ ma{-}interface{-}locs($I$) $\in$ Id)
\\[0ex]$\Rightarrow$ \=($\forall$$k$:\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} .\+
\\[0ex]($k$ $\in$ ma{-}interface{-}dom($I$;$i$) $\in$ Knd)
\\[0ex]$\Rightarrow$ \=(alle{-}at(${\it es}$;$i$;$e$.(es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)\+
\\[0ex]$\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r ma{-}interface{-}valtype($I$;$i$;$k$)))
\\[0ex]\& ($\forall$$x$:Id. es{-}vartype(${\it es}$; $i$; $x$) $\subseteq$r fpf{-}cap(ma{-}interface{-}ds($I$;$i$);IdDeq;$x$;Top))))
\-\-\-
\end{tabbing}